Definitions | {T}, P  Q, x:A. B(x), SQType(T), Id, s = t, Prop, s ~ t, x:A B(x), M.dout(l,tg), x:A B(x), <a,b>, P & Q, P  Q, b, {x:A| B(x) }, IdLnk,  x. t(x), 1of(t), Type, Msg(M), Msg(da), type List, State(ds), locl(a), M.sends(k,s,v), Feasible(D), M.da(a), Case b of inl(x) s(x) ; inr(y) t(y), if b t else f fi, f(x)?z, rcv(l,tg), M.ds(x), S T, f(a), filter(P;l), nil, M.ef(k,x,s,v)?w, destination(l), A,  b, , Unit, left+right, lnk(k), islocal(k), tag(k), act(k), kindcase(k; a.f(a); l,t.g(l;t) ), Knd,  x,y. t(x;y), p  q, S T, d-machine(i;M;dec), w-automaton(T;TA;M), Dsys, mlnk(m), source(l), a = b, x.A(x), M(i), M.Msg, M.state, t T |